Nuprl Lemma : imax-list_wf
0,22
postcript
pdf
L
:
List. 0<||
L
||
imax-list(
L
)
latex
Definitions
imax-list(
L
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
x
,
y
.
t
(
x
;
y
)
,
tl(
l
)
,
hd(
l
)
,
imax(
a
;
b
)
,
i
j
,
A
B
,
A
,
False
,
P
Q
,
Prop
,
||
as
||
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
length
wf1
,
imax
wf
,
hd
wf
,
tl
wf
,
list
accum
wf
origin
L:
List. 0<||L|| 
imax-list(L) 
L: List. 0<||L|| imax-list(L) 
x,y. t(x;y)
j
B
A Qx:A. B(x) T